//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package com.prism.e4.rcp.sparse;

import java.io.FileNotFoundException;
import java.util.List;

import com.prism.e4.rcp.dv.DoubleVector;
import com.prism.e4.rcp.dv.IntegerVector;
import com.prism.e4.rcp.jdd.JDD;
import com.prism.e4.rcp.jdd.JDDNode;
import com.prism.e4.rcp.jdd.JDDVars;
import com.prism.e4.rcp.odd.ODDNode;
import com.prism.e4.rcp.prism.NativeIntArray;
import com.prism.e4.rcp.prism.OpsAndBoundsList;
import com.prism.e4.rcp.prism.PrismException;
import com.prism.e4.rcp.prism.PrismLog;

//----------------------------------------------------------------------------------------------

public class PrismSparse {
	// ----------------------------------------------------------------------------------------------
	// load jni stuff from shared library
	// ----------------------------------------------------------------------------------------------

	static {
		try {
			System.loadLibrary("prismsparse");
		} catch (UnsatisfiedLinkError e) {
			System.out.println(e);
			System.exit(1);
		}
	}

	// ----------------------------------------------------------------------------------------------
	// initialise/close down methods
	// ----------------------------------------------------------------------------------------------

	public static void initialise(PrismLog mainLog, PrismLog techLog) {
		setCUDDManager();
		setMainLog(mainLog);
		setTechLog(techLog);
	}

	public static void closeDown() {
		// tidy up any JNI stuff
		PS_FreeGlobalRefs();
	}

	// tidy up in jni (free global references)
	private static native void PS_FreeGlobalRefs();

	// ----------------------------------------------------------------------------------------------
	// cudd manager
	// ----------------------------------------------------------------------------------------------

	// cudd manager

	// jni method to set cudd manager for native code
	private static native void PS_SetCUDDManager(long ddm);

	public static void setCUDDManager() {
		PS_SetCUDDManager(JDD.GetCUDDManager());
	}

	// ----------------------------------------------------------------------------------------------
	// logs
	// ----------------------------------------------------------------------------------------------

	// main log

	// place to store main log for java code
	private static PrismLog mainLog;

	// jni method to set main log for native code
	private static native void PS_SetMainLog(PrismLog log);

	// method to set main log both in java and c++
	public static void setMainLog(PrismLog log) {
		mainLog = log;
		PS_SetMainLog(log);
	}

	// tech log

	// place to store tech log for java code
	private static PrismLog techLog;

	// jni method to set tech log for native code
	private static native void PS_SetTechLog(PrismLog log);

	// method to set tech log both in java and c++
	public static void setTechLog(PrismLog log) {
		techLog = log;
		PS_SetTechLog(log);
	}

	// ------------------------------------------------------------------------------
	// error message
	// ------------------------------------------------------------------------------

	private static native String PS_GetErrorMessage();

	public static String getErrorMessage() {
		return PS_GetErrorMessage();
	}

	// ----------------------------------------------------------------------------------------------
	// JNI wrappers for blocks of sparse code
	// ----------------------------------------------------------------------------------------------

	// ----------------------------------------------------------------------------------------------
	// probabilistic/dtmc stuff
	// ----------------------------------------------------------------------------------------------

	// pctl bounded until (probabilistic/dtmc)
	private static native long PS_ProbBoundedUntil(long trans, long odd,
			long rv, int nrv, long cv, int ncv, long yes, long maybe, int bound);

	public static DoubleVector ProbBoundedUntil(JDDNode trans, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int bound)
			throws PrismException {
		long ptr = PS_ProbBoundedUntil(trans.ptr(), odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), bound);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl until (probabilistic/dtmc)
	private static native long PS_ProbUntil(long trans, long odd, long rv,
			int nrv, long cv, int ncv, long yes, long maybe);

	public static DoubleVector ProbUntil(JDDNode trans, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe)
			throws PrismException {
		long ptr = PS_ProbUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(),
				cols.array(), cols.n(), yes.ptr(), maybe.ptr());
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl cumulative reward (probabilistic/dtmc)
	private static native long PS_ProbCumulReward(long trans, long sr,
			long trr, long odd, long rv, int nrv, long cv, int ncv, int bound);

	public static DoubleVector ProbCumulReward(JDDNode trans, JDDNode sr,
			JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, int bound)
			throws PrismException {
		long ptr = PS_ProbCumulReward(trans.ptr(), sr.ptr(), trr.ptr(),
				odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(),
				bound);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl inst reward (probabilistic/dtmc)
	private static native long PS_ProbInstReward(long trans, long sr, long odd,
			long rv, int nrv, long cv, int ncv, int time);

	public static DoubleVector ProbInstReward(JDDNode trans, JDDNode sr,
			ODDNode odd, JDDVars rows, JDDVars cols, int time)
			throws PrismException {
		long ptr = PS_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(),
				rows.array(), rows.n(), cols.array(), cols.n(), time);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl reach reward (probabilistic/dtmc)
	private static native long PS_ProbReachReward(long trans, long sr,
			long trr, long odd, long rv, int nrv, long cv, int ncv, long goal,
			long inf, long maybe);

	public static DoubleVector ProbReachReward(JDDNode trans, JDDNode sr,
			JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal,
			JDDNode inf, JDDNode maybe) throws PrismException {
		long ptr = PS_ProbReachReward(trans.ptr(), sr.ptr(), trr.ptr(),
				odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(),
				goal.ptr(), inf.ptr(), maybe.ptr());
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// transient (probabilistic/dtmc)
	private static native long PS_ProbTransient(long trans, long odd,
			long init, long rv, int nrv, long cv, int ncv, int time);

	public static DoubleVector ProbTransient(JDDNode trans, ODDNode odd,
			DoubleVector init, JDDVars rows, JDDVars cols, int time)
			throws PrismException {
		long ptr = PS_ProbTransient(trans.ptr(), odd.ptr(), init.getPtr(),
				rows.array(), rows.n(), cols.array(), cols.n(), time);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// ----------------------------------------------------------------------------------------------
	// nondeterministic/mdp stuff
	// ----------------------------------------------------------------------------------------------

	// pctl bounded until (nondeterministic/mdp)
	private static native long PS_NondetBoundedUntil(long trans, long odd,
			long rv, int nrv, long cv, int ncv, long ndv, int nndv, long yes,
			long maybe, int time, boolean minmax);

	public static DoubleVector NondetBoundedUntil(JDDNode trans, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes,
			JDDNode maybe, int time, boolean minmax) throws PrismException {
		long ptr = PS_NondetBoundedUntil(trans.ptr(), odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				yes.ptr(), maybe.ptr(), time, minmax);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl until (nondeterministic/mdp)
	private static native long PS_NondetUntil(long trans, long trans_actions,
			List<String> synchs, long odd, long rv, int nrv, long cv, int ncv,
			long ndv, int nndv, long yes, long maybe, boolean minmax, long strat);

	public static DoubleVector NondetUntil(JDDNode trans, JDDNode transActions,
			List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols,
			JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax,
			IntegerVector strat) throws PrismException {
		long ptr = PS_NondetUntil(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				yes.ptr(), maybe.ptr(), minmax,
				(strat == null) ? 0 : strat.getPtr());
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl cumulative reward (probabilistic/mdp)
	private static native long PS_NondetCumulReward(long trans, long sr,
			long trr, long odd, long rv, int nrv, long cv, int ncv, long ndv,
			int nndv, int bound, boolean minmax);

	public static DoubleVector NondetCumulReward(JDDNode trans, JDDNode sr,
			JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols,
			JDDVars nondet, int bound, boolean minmax) throws PrismException {
		long ptr = PS_NondetCumulReward(trans.ptr(), sr.ptr(), trr.ptr(),
				odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(),
				nondet.array(), nondet.n(), bound, minmax);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl inst reward (nondeterministic/mdp)
	private static native long PS_NondetInstReward(long trans, long sr,
			long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv,
			int time, boolean minmax, long init);

	public static DoubleVector NondetInstReward(JDDNode trans, JDDNode sr,
			ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, int time,
			boolean minmax, JDDNode init) throws PrismException {
		long ptr = PS_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(),
				rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(),
				nondet.n(), time, minmax, init.ptr());
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// pctl reach reward (nondeterministic/mdp)
	private static native long PS_NondetReachReward(long trans,
			long trans_actions, List<String> synchs, long sr, long trr,
			long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv,
			long goal, long inf, long maybe, boolean minmax);

	public static DoubleVector NondetReachReward(JDDNode trans,
			JDDNode transActions, List<String> synchs, JDDNode sr, JDDNode trr,
			ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet,
			JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax)
			throws PrismException {
		long ptr = PS_NondetReachReward(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, sr.ptr(), trr.ptr(), odd.ptr(),
				rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(),
				nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	private static native double[] PS_NondetMultiObj(long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax,
			long start, long ptr_adversary, long ptr_TransSparseMatrix,
			long[] ptr_yes_vec, int[] probStepBounds,
			long[] ptr_RewSparseMatrix, double[] rewardWeights,
			int[] rewardStepBounds);

	public static double[] NondetMultiObj(ODDNode odd, JDDVars rows,
			JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start,
			NativeIntArray adversary, NDSparseMatrix transSparseMatrix,
			DoubleVector[] yes_vec, int[] probStepBounds,
			NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights,
			int[] rewardStepBounds) throws PrismException {
		long[] ptr_ndsp_r = null;
		if (rewSparseMatrix != null) {
			ptr_ndsp_r = new long[rewSparseMatrix.length];
			for (int i = 0; i < ptr_ndsp_r.length; i++)
				ptr_ndsp_r[i] = (rewSparseMatrix[i] != null) ? rewSparseMatrix[i]
						.getPtr() : 0;
		}

		long[] ptr_yes_vec = null;
		if (yes_vec != null) {
			ptr_yes_vec = new long[yes_vec.length];
			for (int i = 0; i < yes_vec.length; i++)
				ptr_yes_vec[i] = (yes_vec[i] != null) ? yes_vec[i].getPtr() : 0;
		}

		double[] ret = PS_NondetMultiObj(odd.ptr(), rows.array(), rows.n(),
				cols.array(), cols.n(), nondet.array(), nondet.n(), minmax,
				start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(),
				ptr_yes_vec, probStepBounds, ptr_ndsp_r, rewardWeights,
				rewardStepBounds);
		if (ret == null)
			throw new PrismException(getErrorMessage());
		else
			return ret;

	}

	private static native double[] PS_NondetMultiObjGS(long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, boolean minmax,
			long start, long ptr_adversary, long ptr_TransSparseMatrix,
			long[] ptr_yes_vec, int[] probStepBounds,
			long[] ptr_RewSparseMatrix, double[] rewardWeights,
			int[] rewardStepBounds);

	public static double[] NondetMultiObjGS(ODDNode odd, JDDVars rows,
			JDDVars cols, JDDVars nondet, boolean minmax, JDDNode start,
			NativeIntArray adversary, NDSparseMatrix transSparseMatrix,
			DoubleVector[] yes_vec, int[] probStepBounds,
			NDSparseMatrix[] rewSparseMatrix, double[] rewardWeights,
			int[] rewardStepBounds) throws PrismException {
		long[] ptr_ndsp_r = null;
		if (rewSparseMatrix != null) {
			ptr_ndsp_r = new long[rewSparseMatrix.length];
			for (int i = 0; i < ptr_ndsp_r.length; i++)
				ptr_ndsp_r[i] = (rewSparseMatrix[i] != null) ? rewSparseMatrix[i]
						.getPtr() : 0;
		}

		long[] ptr_yes_vec = null;
		if (yes_vec != null) {
			ptr_yes_vec = new long[yes_vec.length];
			for (int i = 0; i < yes_vec.length; i++)
				ptr_yes_vec[i] = (yes_vec[i] != null) ? yes_vec[i].getPtr() : 0;
		}

		double[] ret = PS_NondetMultiObjGS(odd.ptr(), rows.array(), rows.n(),
				cols.array(), cols.n(), nondet.array(), nondet.n(), minmax,
				start.ptr(), adversary.getPtr(), transSparseMatrix.getPtr(),
				ptr_yes_vec, probStepBounds, ptr_ndsp_r, rewardWeights,
				rewardStepBounds);
		if (ret == null)
			throw new PrismException(getErrorMessage());
		else
			return ret;
	}

	// multi-objective (nondeterministic/mdp)
	private static native double PS_NondetMultiReach(long trans,
			long trans_actions, List<String> synchs, long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, long targets[],
			int relops[], double bounds[], long maybe, long start);

	public static double NondetMultiReach(JDDNode trans, JDDNode transActions,
			List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols,
			JDDVars nondet, List<JDDNode> targets,
			OpsAndBoundsList opsAndBounds, JDDNode maybe, JDDNode start)
			throws PrismException {
		// Convert lists to arrays for passing to JNI
		int i, n = targets.size();
		long targetsArr[] = new long[n];
		int relOpsArr[] = new int[n];
		double boundsArr[] = new double[n];
		for (i = 0; i < n; i++) {
			targetsArr[i] = targets.get(i).ptr();
			relOpsArr[i] = opsAndBounds.getProbOperator(i).toNumber();
			boundsArr[i] = opsAndBounds.getProbBound(i);
		}
		double res = // relOps.get(0).intValue()>2 ?
		PS_NondetMultiReach(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				targetsArr, relOpsArr, boundsArr, maybe.ptr(), start.ptr()); // :
		// PS_NondetMultiReach(trans.ptr(), odd.ptr(), rows.array(), rows.n(),
		// cols.array(), cols.n(), nondet.array(), nondet.n(), targetsArr,
		// relOpsArr, boundsArr, maybe.ptr(), start.ptr(), (checkReach? 1 : 0),
		// 0, 0);
		if (res == -1)
			throw new PrismException(getErrorMessage());
		return res;
	}

	private static native double PS_NondetMultiReach1(long trans,
			long trans_actions, List<String> synchs, long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, long targets[],
			long combinations[], int combinationIDs[], int relops[],
			double bounds[], long maybe, long start);

	public static double NondetMultiReach1(JDDNode trans, JDDNode transActions,
			List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols,
			JDDVars nondet, List<JDDNode> targets, List<JDDNode> combinations,
			List<Integer> combinationIDs, OpsAndBoundsList opsAndBounds,
			JDDNode maybe, JDDNode start) throws PrismException {
		// Convert lists to arrays for passing to JNI
		int i, n = targets.size();
		long targetsArr[] = new long[n];
		int relOpsArr[] = new int[n];
		double boundsArr[] = new double[n];
		for (i = 0; i < n; i++) {
			targetsArr[i] = targets.get(i).ptr();
			relOpsArr[i] = opsAndBounds.getProbOperator(i).toNumber();
			boundsArr[i] = opsAndBounds.getProbBound(i);
		}
		long combinationsArr[] = new long[combinations.size()];
		int combinationIDsArr[] = new int[combinationIDs.size()];
		for (i = 0; i < combinations.size(); i++) {
			combinationsArr[i] = combinations.get(i).ptr();
		}
		for (i = 0; i < combinationIDs.size(); i++)
			combinationIDsArr[i] = combinationIDs.get(i);
		double res = // relOps.get(0).intValue()>2 ?
		PS_NondetMultiReach1(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				targetsArr, combinationsArr, combinationIDsArr, relOpsArr,
				boundsArr, maybe.ptr(), start.ptr()); // :
		// PS_NondetMultiReach(trans.ptr(), odd.ptr(), rows.array(), rows.n(),
		// cols.array(), cols.n(), nondet.array(), nondet.n(), targetsArr,
		// relOpsArr, boundsArr, maybe.ptr(), start.ptr(), (checkReach? 1 : 0),
		// 0, 0);
		if (res == -1)
			throw new PrismException(getErrorMessage());
		return res;
	}

	// multi-objective (nondeterministic/mdp)
	private static native double PS_NondetMultiReachReward(long trans,
			long trans_actions, List<String> synchs, long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, long targets[],
			int relopsProb[], double boundsProb[], int relopsReward[],
			double boundsReward[], long maybe, long start, long trr[], long becs);

	public static double NondetMultiReachReward(JDDNode trans,
			JDDNode transActions, List<String> synchs, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDVars nondet, List<JDDNode> targets,
			OpsAndBoundsList opsAndBounds, JDDNode maybe, JDDNode start,
			List<JDDNode> trr, JDDNode becs) throws PrismException {
		// Convert lists to arrays for passing to JNI
		int i;// , n = targets.size();
		long targetsArr[] = new long[targets.size()];
		int relOpsProbArr[] = new int[opsAndBounds.probSize()];
		double boundsProbArr[] = new double[opsAndBounds.probSize()];
		int relOpsRewardArr[] = new int[opsAndBounds.rewardSize()];
		double boundsRewardArr[] = new double[opsAndBounds.rewardSize()];
		long trrArr[] = new long[trr.size()];
		long becsArr = becs.ptr();
		for (i = 0; i < targets.size(); i++)
			targetsArr[i] = targets.get(i).ptr();
		for (i = 0; i < opsAndBounds.probSize(); i++) {
			relOpsProbArr[i] = opsAndBounds.getProbOperator(i).toNumber();
			boundsProbArr[i] = opsAndBounds.getProbBound(i);
		}
		for (i = 0; i < opsAndBounds.rewardSize(); i++) {
			relOpsRewardArr[i] = opsAndBounds.getRewardOperator(i).toNumber();
			boundsRewardArr[i] = opsAndBounds.getRewardBound(i);
		}
		for (i = 0; i < trr.size(); i++)
			trrArr[i] = trr.get(i).ptr();

		double res = // relOps.get(0).intValue()>2 ?
		PS_NondetMultiReachReward(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				targetsArr, relOpsProbArr, boundsProbArr, relOpsRewardArr,
				boundsRewardArr, maybe.ptr(), start.ptr(), trrArr, becsArr); // :
		// PS_NondetMultiReach(trans.ptr(), odd.ptr(), rows.array(), rows.n(),
		// cols.array(), cols.n(), nondet.array(), nondet.n(), targetsArr,
		// relOpsArr, boundsArr, maybe.ptr(), start.ptr(), (checkReach? 1 : 0),
		// 0, 0);
		if (res == -1)
			throw new PrismException(getErrorMessage());
		return res;
	}

	private static native double PS_NondetMultiReachReward1(long trans,
			long trans_actions, List<String> synchs, long odd, long rv,
			int nrv, long cv, int ncv, long ndv, int nndv, long targets[],
			long combinations[], int combinationIDs[], int relopsProb[],
			double boundsProb[], int relopsReward[], double boundsReward[],
			long maybe, long start, long trr[], long becs);

	public static double NondetMultiReachReward1(JDDNode trans,
			JDDNode transActions, List<String> synchs, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDVars nondet, List<JDDNode> targets,
			List<JDDNode> combinations, List<Integer> combinationIDs,
			OpsAndBoundsList opsAndBounds, JDDNode maybe, JDDNode start,
			List<JDDNode> trr, JDDNode becs) throws PrismException {
		// Convert lists to arrays for passing to JNI
		int i;// , n = targets.size();
		long targetsArr[] = new long[targets.size()];
		int relOpsProbArr[] = new int[opsAndBounds.probSize()];
		double boundsProbArr[] = new double[opsAndBounds.probSize()];
		int relOpsRewardArr[] = new int[opsAndBounds.rewardSize()];
		double boundsRewardArr[] = new double[opsAndBounds.rewardSize()];
		long trrArr[] = new long[trr.size()];
		long becsArr = becs.ptr();
		for (i = 0; i < targets.size(); i++)
			targetsArr[i] = targets.get(i).ptr();
		for (i = 0; i < opsAndBounds.probSize(); i++) {
			relOpsProbArr[i] = opsAndBounds.getProbOperator(i).toNumber();
			boundsProbArr[i] = opsAndBounds.getProbBound(i);
		}
		for (i = 0; i < opsAndBounds.rewardSize(); i++) {
			relOpsRewardArr[i] = opsAndBounds.getRewardOperator(i).toNumber();
			boundsRewardArr[i] = opsAndBounds.getRewardBound(i);
		}
		for (i = 0; i < trr.size(); i++)
			trrArr[i] = trr.get(i).ptr();
		long combinationsArr[] = new long[combinations.size()];
		int combinationIDsArr[] = new int[combinationIDs.size()];
		for (i = 0; i < combinations.size(); i++) {
			combinationsArr[i] = combinations.get(i).ptr();
		}
		for (i = 0; i < combinationIDs.size(); i++)
			combinationIDsArr[i] = combinationIDs.get(i);

		double res = // relOps.get(0).intValue()>2 ?
		PS_NondetMultiReachReward1(trans.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				targetsArr, combinationsArr, combinationIDsArr, relOpsProbArr,
				boundsProbArr, relOpsRewardArr, boundsRewardArr, maybe.ptr(),
				start.ptr(), trrArr, becsArr); // :
		// PS_NondetMultiReach(trans.ptr(), odd.ptr(), rows.array(), rows.n(),
		// cols.array(), cols.n(), nondet.array(), nondet.n(), targetsArr,
		// relOpsArr, boundsArr, maybe.ptr(), start.ptr(), (checkReach? 1 : 0),
		// 0, 0);
		if (res == -1)
			throw new PrismException(getErrorMessage());
		return res;
	}

	// ----------------------------------------------------------------------------------------------
	// stochastic/ctmc stuff
	// ----------------------------------------------------------------------------------------------

	// csl time bounded until (stochastic/ctmc)
	private static native long PS_StochBoundedUntil(long trans, long odd,
			long rv, int nrv, long cv, int ncv, long yes, long maybe,
			double time, long mult);

	public static DoubleVector StochBoundedUntil(JDDNode trans, ODDNode odd,
			JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe,
			double time, DoubleVector multProbs) throws PrismException {
		long mult = (multProbs == null) ? 0 : multProbs.getPtr();
		long ptr = PS_StochBoundedUntil(trans.ptr(), odd.ptr(), rows.array(),
				rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), time,
				mult);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// csl cumulative reward (stochastic/ctmc)
	private static native long PS_StochCumulReward(long trans, long sr,
			long trr, long odd, long rv, int nrv, long cv, int ncv, double time);

	public static DoubleVector StochCumulReward(JDDNode trans, JDDNode sr,
			JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, double time)
			throws PrismException {
		long ptr = PS_StochCumulReward(trans.ptr(), sr.ptr(), trr.ptr(),
				odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// steady state (stochastic/ctmc)
	private static native long PS_StochSteadyState(long trans, long odd,
			long init, long rv, int nrv, long cv, int ncv);

	public static DoubleVector StochSteadyState(JDDNode trans, ODDNode odd,
			JDDNode init, JDDVars rows, JDDVars cols) throws PrismException {
		long ptr = PS_StochSteadyState(trans.ptr(), odd.ptr(), init.ptr(),
				rows.array(), rows.n(), cols.array(), cols.n());
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// transient (stochastic/ctmc)
	private static native long PS_StochTransient(long trans, long odd,
			long init, long rv, int nrv, long cv, int ncv, double time);

	public static DoubleVector StochTransient(JDDNode trans, ODDNode odd,
			DoubleVector init, JDDVars rows, JDDVars cols, double time)
			throws PrismException {
		long ptr = PS_StochTransient(trans.ptr(), odd.ptr(), init.getPtr(),
				rows.array(), rows.n(), cols.array(), cols.n(), time);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// ------------------------------------------------------------------------------
	// export methods
	// ------------------------------------------------------------------------------

	// export matrix
	private static native int PS_ExportMatrix(long matrix, String name,
			long rv, int nrv, long cv, int ncv, long odd, int exportType,
			String filename);

	public static void ExportMatrix(JDDNode matrix, String name, JDDVars rows,
			JDDVars cols, ODDNode odd, int exportType, String filename)
			throws FileNotFoundException, PrismException {
		int res = PS_ExportMatrix(matrix.ptr(), name, rows.array(), rows.n(),
				cols.array(), cols.n(), odd.ptr(), exportType, filename);
		if (res == -1) {
			throw new FileNotFoundException();
		} else if (res == -2) {
			throw new PrismException("Out of memory building matrix for export");
		}
	}

	// export mdp
	private static native int PS_ExportMDP(long mdp, long trans_actions,
			List<String> synchs, String name, long rv, int nrv, long cv,
			int ncv, long ndv, int nndv, long odd, int exportType,
			String filename);

	public static void ExportMDP(JDDNode mdp, JDDNode transActions,
			List<String> synchs, String name, JDDVars rows, JDDVars cols,
			JDDVars nondet, ODDNode odd, int exportType, String filename)
			throws FileNotFoundException, PrismException {
		int res = PS_ExportMDP(mdp.ptr(), (transActions == null) ? 0
				: transActions.ptr(), synchs, name, rows.array(), rows.n(),
				cols.array(), cols.n(), nondet.array(), nondet.n(), odd.ptr(),
				exportType, filename);
		if (res == -1) {
			throw new FileNotFoundException();
		} else if (res == -2) {
			throw new PrismException("Out of memory building matrix for export");
		}
	}

	// export sub-mdp, i.e. mdp transition rewards
	private static native int PS_ExportSubMDP(long mdp, long submdp,
			String name, long rv, int nrv, long cv, int ncv, long ndv,
			int nndv, long odd, int exportType, String filename);

	public static void ExportSubMDP(JDDNode mdp, JDDNode submdp, String name,
			JDDVars rows, JDDVars cols, JDDVars nondet, ODDNode odd,
			int exportType, String filename) throws FileNotFoundException,
			PrismException {
		int res = PS_ExportSubMDP(mdp.ptr(), submdp.ptr(), name, rows.array(),
				rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(),
				odd.ptr(), exportType, filename);
		if (res == -1) {
			throw new FileNotFoundException();
		} else if (res == -2) {
			throw new PrismException("Out of memory building matrix for export");
		}
	}

	// ------------------------------------------------------------------------------
	// generic iterative solution methods
	// ------------------------------------------------------------------------------

	// power method
	private static native long PS_Power(long odd, long rv, int nrv, long cv,
			int ncv, long a, long b, long init, boolean transpose);

	public static DoubleVector Power(ODDNode odd, JDDVars rows, JDDVars cols,
			JDDNode a, JDDNode b, JDDNode init, boolean transpose)
			throws PrismException {
		long ptr = PS_Power(odd.ptr(), rows.array(), rows.n(), cols.array(),
				cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// jor method
	private static native long PS_JOR(long odd, long rv, int nrv, long cv,
			int ncv, long a, long b, long init, boolean transpose,
			boolean row_sums, double omega);

	public static DoubleVector JOR(ODDNode odd, JDDVars rows, JDDVars cols,
			JDDNode a, JDDNode b, JDDNode init, boolean transpose,
			boolean row_sums, double omega) throws PrismException {
		long ptr = PS_JOR(odd.ptr(), rows.array(), rows.n(), cols.array(),
				cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums,
				omega);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// sor method
	private static native long PS_SOR(long odd, long rv, int nrv, long cv,
			int ncv, long a, long b, long init, boolean transpose,
			boolean row_sums, double omega, boolean forwards);

	public static DoubleVector SOR(ODDNode odd, JDDVars rows, JDDVars cols,
			JDDNode a, JDDNode b, JDDNode init, boolean transpose,
			boolean row_sums, double omega, boolean forwards)
			throws PrismException {
		long ptr = PS_SOR(odd.ptr(), rows.array(), rows.n(), cols.array(),
				cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums,
				omega, forwards);
		if (ptr == 0)
			throw new PrismException(getErrorMessage());
		return new DoubleVector(ptr, (int) (odd.getEOff() + odd.getTOff()));
	}

	// ----------------------------------------------------------------------------------------------
}

// ------------------------------------------------------------------------------